COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	axiom cons:
C00003 ENDMK
C⊗;
axiom cons:
	∀u v z.(zεcartesian(u,v)≡∃x y. xεu ∧ yεv ∧ z=cons(x,y)),
	∀x y.(car(cons(x,y))=x ∧ cdr(cons(x,y))=y;;